the_w:World, e:E. FairFifo  isrcv(kind(e))  index(e)  ||sends(lnk(kind(e));sender(e))|| 

latex

Definitions	t  T, x:A. B(x), kind(e), isrcv(k), b, x:AB(x), {i..j}, P  Q, FairFifo, E, World, x:AB(x), P & Q, AB, i  j < k, {x:A| B(x) }, , {T}, time(e), lnk(k), match(l;t;t'), x.A(x), #$n, x:A. B(x), False, A, , sender(e), sends(l;e), index(e), mu(f), s = t, snds(l;t), Msg, ||as||, rcvs(l;t), destination(l), Action(i), n-m, -n, n+m, a<b, True, T, Void, P  Q
Lemmas	assert-w-match, w-action wf, ldst wf, w-rcvs wf, length wf1, w-Msg wf, w-snds wf, mu wf, w-match-exists, mu-property, nat wf, le wf, w-match wf, lnk wf, w-time wf, world wf, w-E wf, fair-fifo wf, assert wf, isrcv wf, w-ekind wf